es:ES, Cmd, Rsp:Type, isupdate:(Cmd), Delta:(({c:Cmd| (isupdate(c))}  List)Rsp),
Q:(({c:Cmd| (isupdate(c))}  List){c:Cmd| ((isupdate(c)))} Rsp), In:AbsInterface(Cmd),
Out:AbsInterface(Rsp), Sys:AbsInterface(Cmd List), f:sys-antecedent(es;Sys).
abstract-chain-replication{i:l}(es; Cmd; Rsp; isupdate; In; Out; Sys; f; Delta; Q)   

latex

Up	abstract chain replication
Definitions of Statement	abstract-chain-replication
Definitions	s = t, t  T, ES, Type, , x:AB(x), AbsInterface(A), sys-antecedent(es;Sys), fifo-antecedent(es;Sys;f), E(X), <a, b>, E, b, P  Q, P  Q, x:A  B(x), P & Q, P  Q, x:A. B(x), A, input-forwarding{i:l}(es; Cmd; Sys; isupdate; In; f), x:A. B(x), left + right, {x:A| B(x)} , P  Q, e loc e' , if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), !Void(), False, type List, did-forward(es; Sys; f; e), hd(l), L1  L2, adjacent(T;L;x;y), (x  l), a < b, no_repeats(T;l), chain-consistent(f;chain), f(a), e  X, X(e), loc(e), Id, is-query(In;isupdate;e), a:A fp B(a), strong-subtype(A;B), Top, es-interface-history(es; X; e), filter(P;l), , x:A.B(x), f(x)?z, (e <loc e'), A  B, i  j , ||as||, last(L), , Outcome, #$n, A c B, should-forward(es; In; isupdate; f; a), prior(X), [], nth_tl(n;as), A List, [car / cdr], let x,y = A in B(x;y), t.1, Unit, ff, inr x , tt, inl x , True, Atom$n, e c e', EqDecider(T), IdLnk, EOrderAxioms(E; pred?; info), EState(T), Knd, x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, constant_function(f;A;B), abstract-chain-replication, loc(e), kind(e), SWellFounded(R(x;y)), pred!(e;e'), S  T, suptype(S; T), first(e), pred(e), x.A(x)
Lemmas	es-interface-val wf, filter type, es-causle wf, kind wf, loc wf, first wf, pred! wf, strongwellfounded wf, fifo-antecedent wf, rev implies wf, iff wf, constant function wf, qle wf, cless wf, val-axiom wf, rationals wf, nat wf, Msg wf, kindcase wf, Knd wf, EState wf, EOrderAxioms wf, IdLnk wf, deq wf, event system wf, es-E-interface-subtype rel, true wf, false wf, btrue wf, bfalse wf, unit wf, nth tl wf, should-forward wf, did-forward wf, es-prior-interface wf, input-forwarding wf, no repeats wf, length wf1, l member wf, ifthenelse wf, hd wf, adjacent wf, es-le wf, es-is-interface wf, es-loc wf, last wf, Id wf, sublist wf, es-locl wf, sys-antecedent wf, chain-consistent wf, es-interface-subtype rel, es-interface-val wf2, filter wf, es-interface-history wf, top wf, bool wf, assert wf, es-interface wf, member wf, es-E wf, subtype rel wf, not wf, is-query wf, es-E-interface wf